Inference at * 1 1 1 2 
Iof proof for Lemma decidable implies better:



1. P : 
2. Q : x:P.
3. P
4. Dec(Q)
5. Q  
  (P  Q)  ((P  Q)) 

latex

 by D (-2)  

latex

 1: 

 1: 4. Q
 1: 5. Q  
 1:   (P  Q)  ((P  Q))
 2: 

 2: 4. Q
 2: 5. Q  
 2:   (P  Q)  ((P  Q))
 .

Definitions

Dec(P), P  Q